COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	match.lsp[w84,jmc]	ekl definitions of sublis and match
C00007 ENDMK
C⊗;
match.lsp[w84,jmc]	ekl definitions of sublis and match
∂21-Jan-84  1644	JK   
To:   JMC, JJW    
I have a few new proof files in [prf,jk]:

Subst.lsp[prf,jk] does the definition and properties of subst
Flat.lsp[prf,jk] does the definition and properties of flatten
Mapcar.lsp[prf,jk] does the definition and properties of mapcar on multiple lists
Distin.lsp[prf,jk] does the predicate distinct(a,b,c,..)=a≠b∧a≠c∧b≠c∧... for

axiom of choice
(proof foo)
(trw |(∀x.∃y.A(x,y))⊃(∃f.∀x.A(x,f(x)))| (der))
(∀X.(∃Y.A(X,Y)))⊃(∃F.(∀X.A(X,F(X))))

sublis[pat,alist] ← if at pat
		    then [if isvar pat
			  then {assoc[pat,alist}[λz. if n z
							then error[]
							else d z]
			  else pat]
		    else sublis[a pat,alist].sublis[d pat,alist]

(define fsublis |∀x y.(atom x
	              ⊃ fsublis x
	                  = λa0.if isvar pat
				then (λz.if null z then error() else cdr z)
				     assoc(x,a0))
		    ∧ (fsublis(x.y) = λa0.fsublis(x,a0).fsublis(y,a0))|
(use nsexpdef ue: ((atc.|λx a0.if isvar pat
				then (λz.if null z then error() else cdr z)
				     assoc(x,a0)|)
		   (prc.|λx a0.fsublis(x,a0).fsublis(y,a0)|))))

;justification of flatten
;
(wipe-out)
(get-proofs lispax prf prf jk)
(proof test)

(decl (arb arb1 arb2) (type: |?arbitrary|))
(decl prc (type: |@arb⊗@arb→@arb|))
(decl (dfun atc fun1 fun2) (type: |ground→@arb|))

;now state the (primitive recursive schema) for definition on  ALL
;higher type functionals:
;note the use of the variable type in declarations;
;in this way we can specialize to ANY type.
;thus this axiom is really schema. It is the most general
;induction schema that I can formulate:
;the one with parameters follows trivially.

(axiom
 |∀prc atc.∃dfun.∀x y.(atom x ⊃ dfun(x)=atc(x))∧
 				     (dfun(x.y)=
				       prc(dfun(x),dfun(y)))|)
(label high_order_definition)
 
;now can define flatfun(x)=λy.flat(x,y)
;has to done explicitly since the unifier does not coerce 
;variable types

(define flatfun |∀x y.(atom(x)⊃flatfun(x)=(λY.X.Y))∧
                      (flatfun(X.Y)=(λZ.(flatfun(X))((flatfun(Y))(Z))))|
	(use high_order_definition
	     ue: ((atc.|λx.λy.x.y|)
		  (prc.|λarb1 arb2.λz.arb1(arb2(z))|)) ))
 
(define flat |∀x y.flat(x,y)=(flatfun(x))(y)|)
 
;can verify sexp'ness as usual

(ue ((phi.|λx.∀z.sexp (flatfun(x))(z)|))  sexpinduction
    (open flatfun))
;∀X Z.SEXP (FLATFUN(X))(Z)
(label simpinfo)

;the fact about flat

(trw |∀x y z.(atom(x)⊃flat(x,y)=x.y)∧(flat(x.y,z)=flat(x,flat(y,z)))|
     (open flat flatfun))
;∀X Y Z.(ATOM X⊃FLAT(X,Y)=X.Y)∧FLAT(X.Y,Z)=FLAT(X,FLAT(Y,Z))